| contributor | FMI, Sichere und Zuverlässige Softwaresysteme | ||||||||||||||
| creator |
Gaiser, Andreas
| date |
2007-08-21
| description |
48 pages
|
Fuer explizites und auf Buechiautomatne basierendes
LTL-Model-Checking werden Algorithmen eingesetzt, die akzeptierende
Zyklen im Produktautomat des Systems und des Buechiautomaten der
Negation einer LTL-Formel suchen. Es werden mehrere Algorithmen
untersucht und implementiert, die Model Checking on-the-fly
unterstuetzen. Die Algorithmen lassen sich in zwei Klassen
einteilen, auf verschachtelter Tiefensuche basierende und solche,
deren Funktionsprinzip auf dem Finden von starken
Zusammenhangskomponenten beruht. Die Algorithmen werden mithilfe von
Testmodellen u.a. in Bezug auf Geschwindigkeit und Speicherverbrauch
verglichen, und es werden strukturelle Eigenschaften der
Produktautomaten aufgezeigt, die für die unterschiedliche
Performanz der Algorithmen verantwortlich sind.
| format |
application/pdf
| 669049 Bytes | |
| identifier | http://www.informatik.uni-stuttgart.de/cgi-bin/NCSTRL/NCSTRL_view.pl?id=STUD-2096&engl=1 |
| language | ger |
| publisher | Stuttgart, Germany, Universität Stuttgart |
| relation | Student Thesis No. 2096 |
| source | ftp://ftp.informatik.uni-stuttgart.de/pub/library/medoc.ustuttgart_fi/STUD-2096/STUD-2096.pdf |
| subject | Software Engineering Software/Program Verification (CR D.2.4) |
| Specifying and Verifying and Reasoning about Programs (CR F.3.1) | |
| Discrete Mathematics Graph Theory (CR G.2.2) | |
| Model Checking | |
| Büchiautomat | |
| Leerheitstest | |
| Tarjan-Algorithmus | |
| LTL | |
| depth-first search | |
| title | Vergleich von Algorithmen für den Leerheitstest von Büchiautomaten |
| type | Text |
| Student Thesis |